COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file
C00003 00003	.hd206 FALL 1978
C00007 00004	.LSPFONT
C00008 00005	.cb |Proving|
C00010 00006	.next page
C00013 00007	.next page
C00020 ENDMK
C⊗;
.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file;
.PAGE FRAME 56 HIGH 80 WIDE;
.evenleftborder ← oddleftborder ← 1000;
.area text lines 1 to 56;
.place text;
.
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.
.MACRO hw (DATE) ⊂
.   BEGIN TURNON "←"  NOFILL
←MIDTERM
←DATE
.   TURNOFF END ⊃
.
.itemmac
.
.PORTION MAINPORTION
.
.hd206 FALL 1978
.skip
.hw |October 26|

.cb |Programming|
.skip

	Write LISP programs for each of the functions described below.
The function scan be written in either internal or external notation.  Assume a
reasonable number of functions are system defined (e.g. APPEND, REVERSE, PLUS, etc.)
but when in doubt, write the function yourself.
.BEGIN INDENT 0,6

1.1) ⊗depth[x] is the length of the longest path (from root to leaf) in ⊗x.
 Here ⊗x is an S-expression which represents a binary tree.
The following is one i/o pair which satisfies the function definition.

⊗⊗⊗depth[$$((A . (B . C)) . (E . F))$] = 3   (note B and C are deepest)⊗

1.2) ⊗hb[x,n] is true iff the binary tree represented by the S-expression ⊗x has the
property that it is height balanced for parameter ⊗n.  A binary tree is height
balanced if each node is height balanced with respect to ⊗n.  A node is height
balanced with respect to ⊗n if the longest branch on the left is within ⊗n of the
longest branch on the right.
The following are two i/o pairs which satisfy the funtion definition.

⊗⊗⊗hb[$$((A . B) . (C . D)) 0$] = TRUE (the tree is perfectly balanced)⊗

⊗⊗⊗hb[$$(((A . B) . (C . D)). D) 1$] = FALSE⊗

2) ⊗permutation[u,v] is true iff ⊗v is a permuation of ⊗u.  This means that
the list ⊗v is just a re-arrangement of the list ⊗u.  Note:  it is possible
for an element of ⊗u to appear a multiple number of times in ⊗u.  This is fine
as long as it appears the same number of times in ⊗v.
 The following is one i/o pair which satisfies the function definition.

⊗⊗⊗permutation[$$(A B C C B F G) (G C B B A F C)$] = TRUE⊗

3) ⊗polymult[p1,p2] multiplies two polynomials in one variable together.
The representation of the polynomial 5x↑3 - 3x↑2 + 2 is the list of
coefficients (5 -3 0 2).  The result of ⊗polymult should again be a list of
coefficients with no leading 0's.
The following is one i/o pair which satisfies the function definition.

⊗⊗⊗polymult[$$(3 1 4) (4 1)$] = (12 7 17 4)⊗

.END
.LSPFONT
.basicops 
.next page
.cb |Proving|
.skip

	Given the following function descriptions prove the required theorems.
Be explicit and rigorous in recording your proof.  Justify each individual step
(i.e. function expansion, induction hypothesis, etc.).  The only theorems you may
assume have been previously proved are the associativity of append and that NIL
is the identity for append (on either side).
If you need a lemma, prove it.

.begin  nofill select 2 

⊗⊗	reverse[u] ← ⊗
⊗⊗		qif qn u qthen qNIL⊗
⊗⊗		qelse reverse[qd u] * [qa u . qNIL]⊗

⊗⊗	fringe[x] ← ⊗
⊗⊗		qif qat x qthen [x . qNIL]⊗
⊗⊗		qelse fringe[qa x] * fringe[qd x]⊗

⊗⊗	mirror[x] ← ⊗
⊗⊗		qif qat x qthen x⊗
⊗⊗		qelse mirror[qd x] . mirror[qa x]⊗
.end

1) mirror[mirror[x]] = x

2) fringe[mirror[x]] = reverse[fringe[x]]
.next page
.hd206 FALL 1978
.skip
.cb |Midterm Solutions|
.skip
.cb |Programming|

.begin  nofill select 2 

1.1)
⊗⊗	depth[x] ← ⊗
⊗⊗		qif qat x qthen 0⊗
⊗⊗		qelse 1+max[depth[qa x],depth[qd x]]⊗

1.2)
⊗⊗	hb[x,n] ← ⊗
⊗⊗		qif qat x qthen TRUE⊗
⊗⊗		qelse hb[qa x] ∧ hb[qd x] ∧ abs[depth[qa x]-depth[qd x]]≤n⊗

2)
⊗⊗	permutation[u,v] ← ⊗
⊗⊗		qif qn u qthen qn v⊗
⊗⊗		qelse member[qa u,v] ∧ permutation[qd u,remove[qa u,v]]⊗

⊗⊗	remove[x,v] ← ⊗
⊗⊗		qif x = qa v qthen qd v⊗
⊗⊗		qelse qa v . remove[x,qd v]⊗

3)
⊗⊗	polymult[p1,p2] ← ⊗
⊗⊗		polymult1[p1,reverse[p2],length[p1]+length[p2]-1,1]⊗

⊗⊗	polymult1[p1,rp2,n1,n2] ← ⊗
⊗⊗		qif n1=0 qthen qNIL⊗
⊗⊗		qelse⊗
⊗⊗		 conv[trunc[p1,n1],trunc[rp2,n2]] . polymult1[p1,rp2,n1-1,n2+1]⊗

⊗⊗	conv[u,v] ←⊗
⊗⊗		qif qn u ∨ qn v qthen 0⊗
⊗⊗		qelse [qa u] x [qa v] + conv[qd u,qd v]⊗

⊗⊗	trunc[u,n] ← ⊗
⊗⊗		qif length[u]≤n qthen u⊗
⊗⊗		qelse trunc[qd u,n]⊗

.end
.next page
.cb |Proving|

.begin
.SELECT 6;
.verbatim

1) mirror[mirror[x]] = x

   a) Base Case: x is an atom

	mirror[mirror[x]] = mirror[x]				Def. mirror
			  = x					Def. mirror

   b) Inductive Step: x is an S-expression but not an atom

	mirror[mirror[x]]
		= mirror[mirror[dx] . mirror[ax]]		Def. mirror
		= mirror[mirror[ax]] . [mirror [mirror[dx]]	Def. mirror
		= ax . dx					Induction hyp.
		= x						Def. of a,d,.


2) fringe[mirror[x]] = reverse[fringe[x]]

   a) Base Case: x is an atom

	fringe[mirror[x]] = fringe[x]				Def. mirror
			  = x . NIL				Def. fringe
			  = reverse[x . NIL]			Def. reverse
			  = reverse[fringe[x]]			Def. fringe
 
   b) Inductive Step: x is an S-expression but not an atom

	fringe[mirror[x]]
		= fringe[mirror[dx] . mirror[ax]]		Def. mirror
		= fringe[mirror[dx]] * fringe[mirror[ax]]	Def. fringe
		= reverse[fringe[dx]] * reverse[fringe[ax]]	Induction hyp.
		= reverse[fringe[ax] * fringe[dx]]		lemma 1
		= reverse[fringe[x]]				Def. fringe

Lemma for 2)
  reverse[u*v]=reverse[v] * reverse[u]

   a) Base Case: x is NIL

	reverse[u*v] = reverse[v]				Def. append
		     = reverse[v] * NIL				Ident. of *
		     = reverse[v] * reverse[u]			Def. append

   b) Inductive Step: x is a non-null list

	reverse[u*v] = reverse[au . du * v]			Def. append
		     = reverse[du * v] * [au . NIL]		Def. reverse
		     = [reverse[v] * reverse[du]] * [au . NIL]	Induction hyp.
		     = reverse[v] * [reverse[du] * [au . NIL]]	Assoc. of *
		     = reverse[v] * reverse[u]			Def. reverse
.end